Picks up an external-tags cleanup pass (3be1259f38231e10c40b8fbe0329d2d43d823006):

* deletes dead code (fetchOne, fetchWikidataOne, fetchGerbyOne in Fetch.lean);
* fixes a bug in PRArtifact.lean (workflow-name filter excluded fork PRs);
* fixes the extractDir location for crossref-review --pr;
* drops the unimplemented --build-locally flag from crossref-review;
* ungarbles a docstring comment;
* refreshes README, lakefile (all 3 exes default-target), and CI smoke
  tests (now also exercise crossref-render against hostile input).

No behaviour changes for the orchestrator path; the prebuilt
crossref-render binary that the workflow caches will be rebuilt at this
new SHA on next cache miss.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

The README still described post-comment.sh as cloning external-tags on
every run, but since the mathlib4 workflow_run shim caches the prebuilt
binary, the clone+build path is only the fallback. Step list also missed
the new validation and stale-run-skip steps.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…timeout

Substantive update to the orchestrator. The previous design rendered
every cross-reference tag in any file the PR touched; a 1000-file
maintenance PR would fire on hundreds of unchanged tags. The new design
subtracts a master baseline so only tags this PR actually authored
appear in the comment.

What changed:

* Merge-base baseline diff. Look up the PR's merge-base SHA via the
  GitHub compare API, find the master CI run at that exact commit, and
  download its `crossref-tags-baseline` artifact (uploaded by
  mathlib4#39877). Pass it to crossref-render via --baseline-tsv so
  rows that match a baseline row verbatim are dropped. Missing baseline
  (artifact expired, build never ran) is non-fatal: we skip the
  subtraction and log a warning.

* Per-database tag-shape regex validation. Master mathlib's attribute
  parsers enforce these shapes, but the producer is PR-controlled.
  Defence in depth — a malicious dump emitting a tag like "../../etc"
  is rejected before reaching the renderer.

* Wall-clock timeout on the renderer (180s). Each upstream snippet
  fetch has a 10s curl timeout; this caps total render time regardless
  of row count or upstream latency.

* Pass --strict to crossref-render so producer bugs / malicious
  artifacts can't silently hide rows from the bot comment (malformed
  rows are now a hard error).

* Row-count cap (500) after baseline + regex filtering, as a final
  safety net.

* Bump EXTERNAL_TAGS_SHA to 4634089 to pick up the matching
  --baseline-tsv / --strict / percent-encoded URL changes in
  crossref-render.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…oaden baseline lookup

Three robustness fixes:

* Delete orphaned bot comments. Previously, if a PR initially added a
  cross-reference tag and then the author removed it (or the file
  containing it), the orchestrator would exit cleanly without touching
  the existing bot comment — leaving a stale comment that misrepresents
  the current PR state. All "exit clean, nothing to render" paths now
  delete the prior comment (matched by marker prefix).

* Skip the comment update if the rendered body is byte-identical to the
  existing one. Each PR push otherwise generates an "updated comment"
  notification for subscribers even when nothing changed.

* Drop --branch master from the baseline run lookup. The dump output is
  a function of the elaborated environment at the SHA, so a CI run on
  any branch with that exact head SHA produces an equivalent baseline.
  This handles PRs targeting non-master branches (stacked PRs, PRs
  against nightly-testing, etc.) when the merge-base happens to have a
  CI artifact from another branch.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…dead array

The row cap was being applied to the regex-validated, changed-files-
filtered TSV but BEFORE baseline subtraction. A maintenance PR touching
many files containing existing tags could exceed MAX_FILTERED_ROWS
(500) even though the baseline diff would later reduce the render set
to ~0. That turned innocent refactors into failed privileged checks.

Now the orchestrator subtracts the baseline in shell (one awk pass)
before counting and before invoking the renderer. The cap is applied
to the actual render set. The renderer no longer needs --baseline-tsv
from this orchestrator (we already did it); Cli/Review still uses the
flag directly.

Also dropped the unused TAG_REGEXES associative array — the regexes
are inlined in the case at the validation step, which reads better.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Picks up the bridge-vs-baseline retention clarification in
Crossrefs/PRArtifact.lean's module docstring. No behaviour change.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>